import Mathlib

namespace CNVSReconstruction

/-- Elemento strutturato astratto. -/
abbrev Elem := Fin 3

/-- Codifica informativa astratta dell'elemento. -/
def Info : Elem → Nat
  | 0 => 100
  | 1 => 40
  | 2 => 60

/--
Decomposizione non uniforme.

L'elemento 0 viene decomposto nei frammenti 1 e 2.
Gli altri elementi sono terminali.
-/
def D : Elem → Finset Elem
  | 0 => {1, 2}
  | 1 => {1}
  | 2 => {2}

/--
Ricostruzione astratta coerente con la decomposizione.
Qui modelliamo direttamente la proprietà strutturale:
- D(0) ricostruisce 0;
- D(1) ricostruisce 1;
- D(2) ricostruisce 2.
-/
def RecOfDecomposition : Elem → Elem
  | 0 => 0
  | 1 => 1
  | 2 => 2

/--
Test principale:
la codifica informativa è conservata dalla ricostruzione
della decomposizione.
-/
theorem reconstruction_preserves_information_all :
    ∀ s : Elem, Info (RecOfDecomposition s) = Info s := by
  intro s
  fin_cases s <;> rfl

/--
Test root:
l'elemento 0 conserva informazione dopo ricostruzione.
-/
theorem reconstruction_preserves_information_root :
    Info (RecOfDecomposition 0) = Info 0 := by
  rfl

/--
Non-uniformità informativa dei frammenti della decomposizione di 0.
-/
theorem decomposition_is_non_uniform :
    Info 1 ≠ Info 2 := by
  norm_num [Info]

/--
I frammenti 1 e 2 appartengono alla decomposizione di 0.
-/
theorem fragments_belong_to_root_decomposition :
    (1 : Elem) ∈ D 0 ∧ (2 : Elem) ∈ D 0 := by
  simp [D]

end CNVSReconstruction